\begin{tabbing}
chain{-}replication{-}acks\=\{i:l\}\+
\\[0ex](${\it es}$; ${\it Cmd}$; ${\it Rsp}$; ${\it isupdate}$; ${\it In}$; ${\it Out}$; ${\it Sys}$; ${\it Ack}$; $f$; $g$; ${\it Delta}$; $Q$)
\-\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=fifo{-}antecedent(${\it es}$;${\it Sys}$;$f$) \& fifo{-}antecedent(${\it es}$;${\it Ack}$;$g$)\+
\\[0ex]\& ($\forall$$u$:es{-}E{-}interface(${\it es}$;${\it Sys}$). ($f$($u$) = $u$ $\in$ es{-}E(${\it es}$)) $\Leftarrow\!\Rightarrow$ ($\uparrow$($u$ $\in_{b}$ ${\it In}$)))
\\[0ex]\& (es{-}E{-}interface(${\it es}$;${\it In}$) $\subseteq$r es{-}E{-}interface(${\it es}$;${\it Sys}$))
\\[0ex]\& (es{-}E{-}interface(${\it es}$;${\it Out}$) $\subseteq$r es{-}E{-}interface(${\it es}$;${\it Sys}$))
\\[0ex]\& (es{-}E{-}interface(${\it es}$;${\it Out}$) $\subseteq$r es{-}E{-}interface(${\it es}$;${\it Ack}$))
\\[0ex]\& ($\forall$$e$:es{-}E{-}interface(${\it es}$;${\it In}$). ($\neg$($\uparrow$(${\it isupdate}$(${\it In}$($e$))))) $\Rightarrow$ ($\uparrow$($e$ $\in_{b}$ ${\it Out}$)))
\\[0ex]\& (\=$\forall$$e$:es{-}E{-}interface(${\it es}$;${\it Sys}$).\+
\\[0ex]($\neg$($\uparrow$($e$ $\in_{b}$ ${\it In}$))) $\Rightarrow$ (es{-}loc(${\it es}$; ($f$($e$))) = es{-}loc(${\it es}$; $e$) $\in$ Id) $\Rightarrow$ ($\neg$($\uparrow$($e$ $\in_{b}$ ${\it Out}$))))
\-\\[0ex]\& input{-}forwarding\=\{i:l\}\+
\\[0ex](${\it es}$; ${\it Cmd}$; ${\it Sys}$; ${\it isupdate}$; ${\it In}$; $f$)
\-\\[0ex]\& ($\exists$\=${\it chain}$:\{$e$:es{-}E(${\it es}$)$\mid$ ($\uparrow$($e$ $\in_{b}$ ${\it Sys}$)) $\vee$ ($\uparrow$($e$ $\in_{b}$ ${\it Ack}$))\} $\rightarrow$(Id List)\+
\\[0ex](chain{-}config(${\it es}$;p{-}conditional(${\it Ack}$; ${\it Sys}$);${\it chain}$)
\\[0ex]\& chain{-}consistent(${\it es}$;${\it Sys}$;${\it In}$;${\it isupdate}$;${\it Out}$;$f$;${\it chain}$)
\\[0ex]\& (\=$\forall$$e$:es{-}E{-}interface(${\it es}$;${\it Ack}$).\+
\\[0ex]($\neg$(es{-}loc(${\it es}$; ($g$($e$))) = es{-}loc(${\it es}$; $e$) $\in$ Id))
\\[0ex]$\Rightarrow$ \=(adjacent(Id;${\it chain}$($e$);es{-}loc(${\it es}$; $e$);es{-}loc(${\it es}$; ($g$($e$))))\+
\\[0ex]\& adjacent(Id;${\it chain}$($g$($e$));es{-}loc(${\it es}$; $e$);es{-}loc(${\it es}$; ($g$($e$))))))))
\-\-\-\\[0ex]\& (\=$\forall$$e$:es{-}E{-}interface(${\it es}$;${\it Ack}$).\+
\\[0ex](es{-}loc(${\it es}$; ($g$($e$))) = es{-}loc(${\it es}$; $e$) $\in$ Id) $\Rightarrow$ ($\uparrow$($e$ $\in_{b}$ ${\it Out}$)))
\-\\[0ex]\& ($\forall$$e$:es{-}E{-}interface(${\it es}$;${\it Ack}$). ($\uparrow$($e$ $\in_{b}$ ${\it Out}$)) $\Rightarrow$ ($g$($e$) = $e$ $\in$ es{-}E(${\it es}$)))
\\[0ex]\& (\=$\forall$$e$:es{-}E{-}interface(${\it es}$;${\it Ack}$).\+
\\[0ex]($\uparrow$(($g$($e$)) $\in_{b}$ ${\it Out}$)) $\Rightarrow$ is{-}query(${\it In}$;${\it isupdate}$;$g$($e$)) $\Rightarrow$ ($g$($e$) = $e$ $\in$ es{-}E(${\it es}$)))
\-\\[0ex]\& (\=$\forall$$e$:es{-}E{-}interface(${\it es}$;${\it Out}$).\+
\\[0ex](\=is{-}query(${\it In}$;${\it isupdate}$;$e$)\+
\\[0ex]$\Rightarrow$ (${\it Out}$($e$) = $Q$(filter(${\it isupdate}$;es{-}interface{-}history(${\it es}$; ${\it Sys}$; $e$)),${\it In}$($e$)) $\in$ ${\it Rsp}$))
\-\\[0ex]\& (\=($\neg$is{-}query(${\it In}$;${\it isupdate}$;$e$))\+
\\[0ex]$\Rightarrow$ (${\it Out}$($e$) = ${\it Delta}$(filter(${\it isupdate}$;es{-}interface{-}history(${\it es}$; ${\it Sys}$; $e$))) $\in$ ${\it Rsp}$)))
\-\-\\[0ex]\& (\=$\forall$$e$:es{-}E{-}interface(${\it es}$;${\it Ack}$).\+
\\[0ex]${\it Ack}$($e$) = if $e$ $\in_{b}$ ${\it Out}$ then $\parallel$filter(${\it isupdate}$;${\it Sys}$($e$))$\parallel$ else ${\it Ack}$($g$($e$)) fi  $\in$ $\mathbb{Z}$)
\-\-
\end{tabbing}